a:Id, T:Top, ds:x:Id fp Type, P:Top, init:x:Id fp ds(x)?Void, x:Id, t:Type, v:t.
ds || x : t
 (x  dom(init)  init(x) = v)
 (with ds: ds init: initaction a:T precondition a(v) is P ||+ x : t initially x = v) 

latex

Definitions

x:A. B(x), Top, f(x)?z, P  Q, f || g, x : v, b, x  dom(f), f(x), A ||+ B, with ds: ds init: initaction a:T precondition a(v) is P, x : t initially x = v, P & Q, M1 || M2, ma-frame-compatible(A;B), mk-ma, , M1 ||decl M2, 1of(t), 2of(t), Prop, deq-member(eq;x;L), reduce(f;k;as), false, Y, if b t else f fi, True, t  T, P  Q, P  Q, P  Q, x. t(x), true, b, T, ma-frame-compat(A;B), xdom(f). v=f(x)   P(x;v), M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.bframe(k sends on l), M.rframe(A.sends tfL of k on l), z != f(x)  P(a;z), a:A fp B(a), False, , x(s), Unit, A, , a = b

Lemmas

assert wf, deq-member wf, assert of bor, deq property, fpf-dom wf, fpf-trivial-subtype-top, fpf-cap wf, fpf-join-cap-sq, fpf-single wf, bool wf, eqtt to assert, iff transitivity, bor wf, eq id wf, bfalse wf, false wf, or functionality wrt iff, assert-eq-id, bnot wf, not wf, eqff to assert, assert of bnot, eqof wf, band wf, btrue wf, true wf, squash wf, bnot thru bor, assert of band, and functionality wrt iff, fpf-ap wf, Id wf, id-deq wf, fpf-single-dom, fpf-ap-single, fpf-compatible wf, fpf wf, top wf